{-# LANGUAGE TypeFamilies, FlexibleContexts, Rank2Types, QuasiQuotes,
  TypeOperators, ScopedTypeVariables, GADTs, FlexibleInstances,
  MultiParamTypeClasses, UndecidableInstances, TemplateHaskell #-}

{- |

Module      :  Type.Yoko.Fun
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

Maintainer  :  nicolas.frisby@gmail.com
Stability   :  experimental
Portability :  see LANGUAGE pragmas (... GHC)

An explicit perspective on (both parametric and ad-hoc) polymorphic
functions. The datatype representing such a function must be of kind @* -> *@;
the parameter is the type at which the function is to be instantiated.

-}

module Type.Yoko.Fun
  (Domain(..), Dom, Rng, applyU, apply,
   YieldsArrowTSSU, DomF, RngF, eachArrow,
   AsComp(..), WrapComp, WrapCompF
  ) where

import Type.Yoko.Type
import Type.Yoko.SetModel
import Type.Yoko.SetModelTH
import Type.Yoko.Natural




-- | @Domain fn@ is the set of types at which @fn@ can be applied; it's the
-- type-level domain of @fn@.
data Domain fn t where
  AppBy :: (t ::: Domain fn, True ~ (t ::? Domain fn)) =>
           (fn t -> Dom fn t -> Rng fn t) -> Domain fn t

instance SetModel (Domain fn) where evidence AppBy{} x = x

-- | @Dom fn t@ is the domain of @fn@ at type @t@; it's the term-level domain
-- of @fn@ at @t@.
type family Dom (fn :: * -> *) t
-- | @Rng fn t@ is the range of @fn@ at type @t@; it's the term-level range of
-- @fn@ at @t@.
type family Rng (fn :: * -> *) t

-- | @applyD@ is analogous to '$'.
applyU :: Domain fn t -> fn t -> Dom fn t -> Rng fn t
applyU (AppBy f) = f

-- | @apply = applyU membership@.
apply :: (t ::: Domain fn) => fn t -> Dom fn t -> Rng fn t
apply = applyU membership



-- | Used by @YieldsArrowTSSU fn@ to structure the domain of @fn@.
type family DomF (fn :: * -> *) :: * -> *
-- | Used by @YieldsArrowTSSU fn@ to structure the range of @fn@.
type family RngF (fn :: * -> *) :: * -> *

-- | @YieldsArrowTSSU fn@ also gaurantees that @fn@ at @t@ yields a type of the
-- shape @(DomF fn) t -> (RngF fn) t@; i.e. it guarantees that @Dom fn t@ and
-- @Rng fn t@ both don't depend on @t@ and also are an application of a @* ->
-- *@ to @t@.
data YieldsArrowTSSU fn t where
  YieldsArrowTSSU ::
    (Dom fn t ~ DomF fn t, Rng fn t ~ RngF fn t
    ) => Domain fn t -> YieldsArrowTSSU fn t
obvious_membership ''YieldsArrowTSSU

instance SetModel (YieldsArrowTSSU fn) where
  evidence (YieldsArrowTSSU u) x = evidence u x

-- | Just a specialization: @yieldsArrowTSSU (YieldsArrowTSSU domD) fn = applyU domU fn@.
yieldsArrowTSSU :: (forall t. fn t) -> YieldsArrowTSSU fn t -> DomF fn t -> RngF fn t
yieldsArrowTSSU fn (YieldsArrowTSSU domU) = applyU domU fn

-- | Defines an @'NT' u@ from a suitably polymorphic type-function @fn@ if @u@
-- is finite and the function yields an arrow at each type in @u@.
eachArrow :: forall fn u.
  (u :=> YieldsArrowTSSU fn
  ) => (forall t. fn t) -> NT u (ArrowTSS (DomF fn) (RngF fn))
eachArrow fn = NT $ yieldsArrowTSSU fn . weaken





type instance t ::? Domain (fn :. f) = f t ::? Domain fn

type instance Dom (fn :. f) a = Dom fn (f a)
type instance Rng (fn :. f) a = Rng fn (f a)
type instance DomF (fn :. f) = DomF fn
type instance RngF (fn :. f) = RngF fn
instance (f t ::: Domain fn) => t ::: Domain (fn :. f) where
  membership = AppBy $ \(Compose fn) -> apply fn





-- | Only instance: @type instance WrapComp (f (g a)) = (f :. g) a@.
type family WrapComp a
type instance WrapComp (f (g a)) = (f :. g) a

-- | Only instance: @type instance WrapCompF (f (g a)) = f :. g@.
type family WrapCompF a :: * -> *
type instance WrapCompF (f (g a)) = f :. g





{- | Defining instances:

@
  type instance Dom (AsComp fn) t = WrapComp (Dom fn t)
  type instance Rng (AsComp fn) t = WrapComp (Rng fn t)
  membership = AppBy $ \(AsComp fn) -> wrap . apply fn . unwrap
@

-}
newtype AsComp (fn :: * -> *) t = AsComp (fn t); wraps_thinly ''AsComp

type instance t ::? Domain (AsComp fn) = t ::? Domain fn

type instance Dom (AsComp fn) t = WrapComp (Dom fn t)
type instance Rng (AsComp fn) t = WrapComp (Rng fn t)

type instance DomF (AsComp fn) = WrapCompF (Dom fn ())
type instance RngF (AsComp fn) = WrapCompF (Rng fn ())

instance (t ::: Domain fn,
          Dom fn t ~ ex0 (ex1 ex2), Rng fn t ~ ex3 (ex4 ex5)
         ) => t ::: Domain (AsComp fn) where
  membership = AppBy $ \(AsComp fn) -> wrap . apply fn . unwrap
